Here we investigate \emph{safety} and \emph{consistency}, the main properties of our typing system.
While safety (discussed in Sect.~\ref{ss:safety}) corresponds to the expected guarantee of adherence to prescribed session types and absence of runtime errors, 
consistency (discussed in Sect.~\ref{ss:consist})  formalizes a correct interplay between communication actions and update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.
These are classic ingredients in session types presentations (see, e.g., \cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07});
our notions generalize usual definitions 
to the case in which processes which may interact even if contained in arbitrarily nested transparent locations (formalized by the contexts of 
Def.~\ref{d:context}).

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa$, i.e., 
$P$ is one of the following:
$$
%\begin{array}{llcllcrl}
%  &  \inC{\kappa^{\,p}}{\tilde{x}}.P' & &  & \outC{\kappa^{\,p}}{v}.P' & &    &  \close{\kappa^{\,p}}.P'  \\
%  &   \catch{\kappa^{\,p}}{x}.P' & &  &    \throw{\kappa^{\,p}}{d^{\,q}}.P' \\
%  &   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m} ~~ & &  &   \select{\kappa^{\,p}}{n}.P' 
%\end{array}
\begin{array}{ll}
    \inC{\kappa^{\,p}}{\tilde{x}}.P' & \outC{\kappa^{\,p}}{v}.P'    \\
  \catch{\kappa^{\,p}}{x}.P' &  \throw{\kappa^{\,p}}{k^{\,q}}.P' \\
   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m}  &   \select{\kappa^{\,p}}{n}.P' \\
    \close{\kappa^{\,p}}.P' & 
\end{array}
$$
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities, i.e., 
for some contexts $C$, $D$, and $E$,
$P$ is 
structurally congruent to
one of the following:
$$
\begin{array}{c}
(\nu \tilde{\kappa})(E\big\{C\{\inC{\kappa^{\,p}}{\tilde{x}}.P_1\} \para D\{\outC{\kappa^{\,\overline{p}}}{v}.P_2\}\big\}  )\\  
(\nu \tilde{\kappa})(E\big\{C\{\catch{\kappa^{\,p}}{x}.P_1\} \para  D\{\throw{\kappa^{\,\overline{p}}}{k^{\,q}}.P_2\} \big\}) \\
(\nu \tilde{\kappa})(E\big\{C\{\branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \cdots \parallel n_m{:}P_m} \} \para  D\{  \select{\kappa^{\,\overline{p}}}{n_i};P'\}\big\} )  \\
(\nu \tilde{\kappa})(E\big\{C\{\close{\kappa^{\,p}}.P_1\}  \para  D\{\close{\kappa^{\,\overline{p}}}.P_2\}\big\})
\end{array}
$$
We say a $\kappa$-redex is \emph{located} if one or both of its $\kappa$-processes is inside at least one located process.

$P$ is an \emph{error} if
$P \equiv (\nu \tilde{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
%exactly one $\kappa$-process
%\underline{or}
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}




\subsection{Session Safety}\label{ss:safety}


We now give
subject congruence and subject reduction results for our typing discipline.
Together with some 
some auxiliary results, these provide the basis for the proof of type safety (Theorem~\ref{t:safety} in Page~\pageref{t:safety}).
We start by giving three standard results, namely weakening, strengthening, and channel lemmas.


\begin{lemma}[Weakening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.  If $\mathsf{X} \notin vdom(\Theta)$ then $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}


\begin{lemma}[Strengthening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.
If $\mathsf{X}  \notin \mathsf{fv}(P)$ then $\judgebis{\env{\Gamma}{ \Theta \setminus \mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}



\begin{lemma}[Channel Lemma]\label{lem:channel}
  Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, 
 $\cha \notin \mathsf{fc}(P) \cup \mathsf{bc}(P)$ iff $\cha \notin dom(\ActS)$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}

We are ready to show the Subject Congruence Theorem:

\begin{theorem}[Subject Congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule.

%\begin{description}
\paragraph{\bf Case $\restr{\cha}{ ( \compo{l}{h}{P})  } \equiv   \compo{l}{h}{ \restr{\cha}{P}  }$} \quad \\
We examine the left to right direction:
we show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{ ( \compo{l}{h}{P} ) }}{\type{\ActS}{\INT}}$ 
then 
$\judgebis{\env{\Gamma}{\Theta}}{  \compo{l}{h}{\restr{\cha}{P}  }}{\type{\ActS}{\INT}}$.
Since $\restr{\cha}{  (\compo{l}{h}{P} ) }$ is well-typed, 
by inversion on rules \rulename{t:Loc} and \rulename{t:CRes}, 
for some $\ST, \Delta'$
we have:
$$
\cfrac{
\begin{array}{c}
\Theta \vdash l:\INT' \\
\INT \sqsubseteq \INT'
\end{array}
\quad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } \quad
 h = | \ActS', \cha^-:\ST, \cha^+:\overline{\ST} |  
}{\cfrac{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{P} }{ \type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}} {\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(\compo{l}{h}{P})}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$ 
%\jp{perhaps this is redundant:} 
Hence $ \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT}}$, 
where $\ActS = \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Now, starting from $P$, and by applying first rule  \rulename{t:CRes} and then rule  \rulename{Loc} we obtain: 
$$
\cfrac
{
\cfrac{
 \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS', \cha^-:\ST, \cha^+:\overline{\ST}}{\INT} } 
}
{ 
\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT}}}
\ 
\begin{array}{c}
\Theta \vdash l:\INT' \qquad \INT \sqsubseteq \INT' \\
 h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| 
\end{array}
}
{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{h}{\restr{\cha}{P}} }{ \type{\ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]}{\INT}}}
$$
Observe that 
$h = | \ActS', [\cha^-:\ST], [\cha^+:\overline{\ST}]| =  | \ActS', \cha^-:\ST, \cha^+:\overline{\ST}|$---bracketing does not influence $h$, i.e.,
The reasoning for the right to left direction is analogous and omitted.


\paragraph{\bf Case $P \para \nil  \equiv P $} \quad \\ 
We examine only the left to right direction; the converse direction is similar. 
We then show that if  $\judgebis{\env{\Gamma}{\Theta}}{P \para \nil }{\type{\ActS}{\INT}}$
then  $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{\INT}}$.
 By inversion on rule \rulename{t:Par}  there exist $\Delta_1, \INT_1$ such that $$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{\INT_1}} \text{ and }  \judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}$$
with  $\ActS= \ActS_1 \cup \emptyset = \ActS_1$ and $\INT = \INT_1 \uplus \emptyset = \INT_1$ and so the thesis follows.




\paragraph{\bf Case $\restr{\cha}{P} \para Q \equiv \restr{\cha}{(P \para Q)}$ with $\cha \notin \mathsf{fc}(Q) $} \quad \\
We examine only the right to left direction; the other direction is analogous.
We show that if 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{(P \para Q)}}{\type{\ActS}{\INT}}$ (with $\cha \notin \mathsf{fc}(Q)$) then 
also 
$\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{P \para Q}}{\type{\ActS}{\INT}}$.
By inversion on rules 
\rulename{t:CRes} and \rulename{t:Par}
we have:
$$
\cfrac{
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 \qquad
 \INT = \INT_1 \addelta \INT_2}
{ \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2, \cha^-:\ST, \cha^+:\overline{\ST} }{\INT'}}}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{(P\para Q)}}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}}
$$
where $\ActS = \ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]$.
Observe how in the inversion of rule \rulename{t:Par} we have used assumption 
$\cha \notin \mathsf{fc}(Q) \cup \mathsf{bc}(Q)$  and Lemma \ref{lem:channel}  to infer 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}$ and $ \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}$. Now, % and we can construct the following derivation tree
using first rule  \rulename{t:CRes} and then rule  \rulename{t:Par} we have:
 $$
\cfrac{ 
\cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1,  \cha^-:\ST, \cha^+:\overline{\ST} }{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS_1, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT_1 }}}
\quad 
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
\\
 \INT = \INT_1 \addelta \INT_2
\end{array}
 } 
{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}\para Q}{\type{\ActS_1 \cup \ActS_2, [\cha^-:\ST], [\cha^+:\overline{\ST}]}{ \INT }}}
$$
%The converse is similar.

\paragraph{\bf Case $\restr{\cha}{ \nil  } \equiv \nil$ } \quad \\ This case is easily proven by appealing to rule \rulename{t:Weak}.


\paragraph{\bf Cases $P \para Q  \equiv Q \para P$ and $(P \para Q )\para R \equiv P \para (Q \para R)$} \quad \\ 
In both cases, the proof  follows by commutativity and associativity of $\cup$ and $\uplus$ (cf. Def.~\ref{d:interf}).

\paragraph{\bf Case $\restr{\cha}{\restr{\cha'}{P}} \equiv \restr{\cha'}{\restr{\cha}{P}}$} \quad \\  This case is similar to previous ones.
%\end{description}
\end{proof}

The following auxiliary result concerns substitutions for channels, expressions, and process variables.
Observe how the case of process variables has been relaxed so as to allow substitution 
with a process with ``smaller'' interface (in the sense of \intpr). This extra flexibility is in line
with the typing rule for located processes (rule~\rulename{t:Loc}), and will be useful later on in proofs.
%In order to prove the subject reduction theorem we need some auxiliary results. The first lemma handles substitutions.

\begin{lemma}[Substitution Lemma]\label{lem:substitution}
\quad 
\begin{enumerate}
 \item \label{subchavar}If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS,x:\ST}{\INT}}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS, \cha^p:\ST }{\INT}}$ %\jp{This statement should be different, I think.} \todo{check if this new formulation" is what you were thinking} 
  \item \label{subvalvar}If $\judgebis{\env{\Gamma, \tilde{x}:\tilde{\tau}}{ \Theta}}{P}{\type{\ActS}{\INT}}$ and $\Gamma \vdash \tilde{e}:\tilde{\tau}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\tilde{e}}{\tilde{x}}}{\type{\ActS}{\INT}}$. 
 % \item If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS}{\INT}}$  then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS\sub{\cha^p}{x}}{\INT}}$. 
   \item \label{subprovar} If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT}}{P}{\type{\emptyset}{\INT_1}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\emptyset}{\INT'}}$ with $\INT' \sqsubseteq \INT$  then \\ 
   $\judgebis{\env{\Gamma}{\Theta}}{P\sub{Q}{\mathsf{X}}}{\type{\emptyset}{\INT'_1}}$ with $\INT'_1 \sqsubseteq \INT_1$. %\jp{in the proof, it'd be better to explain why this inequality holds}
\end{enumerate}
\end{lemma}
\begin{proof}
Easily shown by induction on the structure of $P$.
\end{proof}
 
As reduction may occur inside contexts, in proofs it is useful to refer to the 
 %Then, we need to introduce how to manipulate contexts, to this aim we define the 
 type of the processes inside a context.

\begin{definition}[Type of contexts]
Let $C$ be a context as in Def.~\ref{d:context}. 
The type of $C$, denoted $\typecontx{C}{ \Gamma}{ \Theta}$, is 
inductively defined as a pair:
$$
\begin{array}{ll}
 \typecontx{\bullet}{ \Gamma}{ \Theta} &= (\emptyset, \emptyset)\\
 \typecontx{\compo{l}{h}{C \para P}}{ \Gamma}{ \Theta}& = (\Pi_1( \typecontx{C}{\Gamma}{ \Theta}) \cup \ActS, ~\Pi_2(\typecontx{C}{\Gamma}{ \Theta}) \addelta \INT) \qquad \qquad \qquad \ \\
  & \hfill \text{ if } ~\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}
\end{array}
$$
where $\Pi_1(\typecontx{C}{ \Gamma}{ \Theta})$ 
(resp. $\Pi_2(\typecontx{C}{ \Gamma}{ \Theta})$)
denote the first (resp. second) element of pair 
$\typecontx{C}{ \Gamma}{ \Theta}$.
\end{definition}

%\todo{Cambiare notazione $\typecontx{C}{ \Gamma}{\Theta}$}
Next we state how to infer the type of a context:

\begin{lemma}\label{lem:context}
 Let  $P$ be a process and $C$ a context as in Def.~\ref{d:context}. Then \\ $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}}$ and $\typecontx{C}{ \Gamma}{ \Theta} = (\ActS_C, \INT_C) $ iff 
$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_C \cup \ActS_P}{\INT_C \addelta \INT_P}}$
\end{lemma}
\begin{proof}
By induction on the structure of the context $C\{\bullet\}$. The proof for the $(\Rightarrow)$ directions follows by observing that the only rules applied for typing $C\{P\}$ are  \rulename{t:Loc} and \rulename{t:Par} that either do not  change or can  only extend $\ActS_P$ and $\INT_P$. The opposite direction $(\Leftarrow)$, similarly, relies on the typing inversion on the same rules
 \rulename{t:Loc} and \rulename{t:Par}.
\end{proof}


\begin{newnotation}
In the proof of Theorem~\ref{th:subred}, we shall use the following notation 
to denote an use of  Lemma \ref{lem:context}:
$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_P, \ActS_C}{ \INT_P \uplus \INT_C}}}		  
    {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{ \INT_P }}}
$$
\end{newnotation}




%\jp{Now I tend to think that we may need something like Lemma \ref{lem:context}. 
%The point is that in the proof we would like to get rid of contexts, justifying the ellipses (not to enclose processes within contexts, as Lemma 9 does). 
%With such a lemma, we could "go up" in the typing tree until we have something without contexts.
%At that point, we apply something (say, a substitution lemma). Then, we conclude by "going down" again, reconstructing the context. The proof would be indeed by structural induction on the context (base case: empty contexts--trivial; cases for locations/restriction are easy by IH and typing inversion).}

%\jp{Why not writing this as a corollary?}
%\todo{Maybe just a remark}
% Notice that previous lemma allows us to conclude that, given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\ActS}{\INT}$ then there exists $\Gamma, \Theta, \ActS', \INT'$ such that $\judgement{\Gamma}{\Theta}{P}{\ActS'}{\INT'}$.


%\todo{Subject reduction works for balanced environments; we need to introduce that notion. }

\begin{definition}[Balanced Typings]\label{d:balanced}
We say a typing 
$\ActS$ is balanced iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $[\kappa^p:\ST] \in \ActS$)
then also 
$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$ (resp. $[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$).
%for all $\kappa^p:\ST \in \ActS$ then also 
%$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$, and 
%for all $[\kappa^p:\ST] \in \ActS$ then also
%$[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$.
\end{definition}

The final requirement for proving that typing ensures safety is the subject reduction theorem below.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}


\begin{proof}
We assume that $\tilde{e} \downarrow \tilde{c}$ is a type preserving operation, for every $\tilde{e}$.
The proof proceeds by induction on the rule applied in the reduction. 
%\begin{description}
\paragraph{\bf Case \rulename{r:Open}}
\begin{multline*} 
E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} \pired  \\
E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }\big)\big\} } 
\end{multline*}
The assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\} }{\type{\ActS}{\INT}}$
is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
inversion on rules \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\}}{\type{\ActS}{\INT}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}}{\type{\ActS'}{\INT'}}}
{    (\ref{eq:typeaccept})
%
&
%
(\ref{eq:typerequest})
}}
$$
where subtrees (\ref{eq:typeaccept}) and (\ref{eq:typerequest}) are as follows:
\begin{equation}\label{eq:typeaccept}
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta \inter{a}{\ST}{1} }}}		  
    { 
 	\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P_1}{\type{\ActS_1}{ \INT_1\addelta \inter{a}{\ST}{1} }}}
  {\Gamma \vdash a: \langle \ST , \overline{\ST } \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}} }}
\end{equation}


\begin{equation}\label{eq:typerequest}
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\Gamma \vdash a: \langle \ST , \overline{\ST} \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
 \end{equation}


By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, and $\ActS' \subseteq \ActS$ where $\ActS' = \ActS'_1 \cup \ActS'_2$. Moreover, we infer $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, and $\INT' \sqsubseteq \INT$ where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{1}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on $P_1$ and $P_2$, we have:
 \begin{itemize}
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{itemize}
By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} we may then reconstruct the derivation leading to contexts $C, D$, and $E$. Let 
$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
\begin{equation}\label{eq:typeacceptsub}
\infer={\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' }}}		  
    { 
    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}}
\end{equation}
and
\begin{equation}\label{eq:typerequestsub}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
we thus obtain:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{R} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{R}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \cup \INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{R }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \cup \INT_2'}}}{
(\ref{eq:typeacceptsub})
%
&
%
	(\ref{eq:typerequestsub})
}
}}
$$
where by Lemma \ref{lem:context}, we have $\INT'' \sqsubseteq \INT_1' \cup \INT_2'$ and 
thus concluding this case. 

\paragraph{\bf Case \rulename{r:ROpen}} 
\begin{multline*}
          E\big\{C\{\repopen{a}{x}.P_1\}  \para  D\{\nopenr{a}{y}.P_2\} \big\}  \pired  \\
E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1 \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} }\big)}\big\}  
         \end{multline*}

The assumption $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} }{\type{\ActS}{\INT}}$ is obtained by the following derivation tree using Lemma \ref{lem:context}($\Leftarrow$) three times and inversion on  rules \rulename{t:RepAccept}, \rulename{t:Request}, and \rulename{t:Par}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\}}{\type{\ActS}{\INT}}}
{ \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}}{\type{\ActS'}{\INT'}}}
{
(\ref{eq:bangaccept})
%
&
%
(\ref{eq:bangrequest})
}}
$$
where (\ref{eq:bangaccept}) and (\ref{eq:bangrequest}) correspond to the subtrees:
\begin{equation}\label{eq:bangaccept}
	\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta \inter{a}{\ST}{\infty} }}}		  
    { 
    	\infer{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{\unres( \INT_1)\addelta \inter{a}{\ST}{\infty} }}}
  {\Gamma \vdash a: \langle \ST , \overline{\ST } \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{x:\ST}{\INT_1}} }}
\end{equation}
\begin{equation}\label{eq:bangrequest}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_2 \}}{ \type{\ActS'_2}{ \INT'_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_2}{ \type{\ActS_2}{ \INT_2\addelta \inter{a}{\overline{\ST}}{1} }}}
	{\Gamma \vdash a: \langle \ST , \overline{\ST} \rangle &
\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
}
\end{equation}


where by Lemma~\ref{lem:context} ($\Leftarrow$) we have  $\ActS_2 \subseteq \ActS_2'$,  $\ActS' \subseteq \ActS$, and $\ActS' = \ActS'_1 \cup \ActS'_2$. Moreover, $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$ and $\INT' \sqsubseteq \INT$ where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{\infty}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
 Now, applying Lemma~\ref{lem:substitution}(\ref{subchavar}) to $P_1$ and $P_2$, we have:
 \begin{itemize} %[$-$]
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\INT_1}}$.
 \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
 \end{itemize}
We also have that $\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{ \INT_1\unres \addelta \inter{a}{\ST}{\infty} }}$.
By applying Lemma~\ref{lem:context} ($\Rightarrow$) and typing rules \rulename{t:Par} and \rulename{t:CRes} we obtain the following derivation trees. Let $R = P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1$
by using rule \rulename{t:Par} and by noticing that $\INT_1\unres \addelta \INT_1 = \INT_1\unres  $ we know that 
$$\judgebis{\env{\Gamma}{\Theta}}{R}{\type{\cha^+:\ST}{ \unres(\INT_1)\addelta \inter{a}{\ST}{\infty} }}$$
Hence by defining:
$$
Q \triangleq C^{+}_{}\{R \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} ,
$$
\begin{equation}\label{eq:bangacceptsub}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{R\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' \addelta \inter{a}{\ST}{\infty}}}}		  
    { 
    	\judgebis{\env{\Gamma}{ \Theta}}{R}{ \type{\cha^+:\ST}{ \unres(\INT_1)\addelta \inter{a}{\ST}{\infty} }}}
\end{equation}
and
\begin{equation}\label{eq:bangrequestsub}
 	\infer={\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_2\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
	{\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
\end{equation}
we have:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{}\big\{\restr{\cha}{Q}\big\}  }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT'' \addelta \inter{a}{\ST}{\infty}}}}
{
	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{Q}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT'_2 \addelta \inter{a}{\ST}{\infty}}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{{Q }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT'_2 \addelta \inter{a}{\ST}{\infty}}}}{
(\ref{eq:bangacceptsub}) %
&
%
(\ref{eq:bangrequestsub})
}
}}
$$
thus concluding this case. 

\paragraph{\bf Case \rulename{r:Upd}} 
$$E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\} 
\pired   
E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$$
The assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\}}{ \type{\ActS}{\INT}}$ is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  
inversion on rules \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc}:
$$
\infer=
{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}\big\}}{ \type{\ActS}{\INT}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{X}\}}{ \type{\ActS_1 \cup \ActS_2}{\INT_2' \addelta \INT_4'}}}
{
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} }{ \type{\ActS_1}{\INT_2'}}}
{\infer{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{0}{P_1}}{ \type{\emptyset}{\INT_2}}}
{ \begin{array}{c}
  \Theta \vdash l:\INT_1\\
   \INT_2 \sqsubseteq \INT_1
   \end{array}
  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\emptyset}{\INT_2} }   }}
&
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\adapt{l}{P_2}{X}\}}{ \type{\ActS_2}{\INT_4'}}}{
\infer{\judgebis{\env{\Gamma}{\Theta}}{ \adapt{l}{P_2}{X}}{ \type{\emptyset}{\emptyset}}}
{\Theta \vdash l:\INT_1  &  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P_2}{\type{\emptyset}{ \INT_3 }}}}
}}
$$
By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \cup \ActS_2 \subseteq \ActS$, $\INT_2 \sqsubseteq \INT_2'$, $\INT_4 \sqsubseteq \INT_4'$, and $\INT_2' \addelta \INT_4' \sqsubseteq \INT$. 
By Lemma \ref{lem:substitution}(\ref{subprovar}) we have  $\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}$ with $\INT'_3 \sqsubseteq \INT_3$, thus process $E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$ can be typed by means of Lemma~\ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}:

$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}}{ \type{\ActS}{\INT'}}}{
\infer
{\judgebis{\env{\Gamma}{\Theta}}{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}}{ \type{\ActS_1 \cup \ActS_2}{\INT''_3 \addelta \INT_4'}}}
{\infer={\judgebis{\env{\Gamma}{\Theta}}{ C\{P_2\sub{P_1}{\mathsf{X}}\} }{\type{\ActS_1}{\INT''_3}}}{
\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}}
&
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS_2}{\INT_4'}}}{
\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
}}
$$
where by Lemma \ref{lem:context}($\Rightarrow$) we know $\INT_3'' \sqsubseteq \INT'_3$ and $\INT_3'' \addelta \INT_4' \sqsubseteq \INT'$.
This concludes the analysis for this case.

\paragraph{\bf Case \rulename{r:I/O}} 
$$E\big\{C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}\big\} 
\pired 
E\big\{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}\big\} \quad (\tilde{e} \downarrow \tilde{c})$$
The assumption is $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}$ with $\ActS$ balanced and we thus obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we let
$$
R \triangleq C\{\outC{\cha^{\,p}}{\tilde{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\tilde{x}}.P_2\}
$$
$$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E\big\{R\big\} }{ \type{\ActS}{\INT}}}
{\infer
{
\judgebis{\env{\Gamma}{\Theta}}{R} {\type{\ActS_1' \cup \ActS_2', \cha^p:!(\tilde{\capab}).{\ST}, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
{ (\ref{eq:out})
&
(\ref{eq:in})
}}
$$
where subtrees (\ref{eq:out}) and (\ref{eq:in}) are as follows:
\begin{equation}\label{eq:out} 
\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{\tilde{e}}.P_1\} } {\type{\ActS_1',  \cha^p:!(\tilde{\capab}).{\ST} }{ \INT_1' }}}{
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{\tilde{e}}.P_1}{\type{\ActS_1, \cha^p:!(\tilde{\capab}).{\ST}}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash \tilde{e}:\tilde{\capab}}}
\end{equation}
\begin{equation}\label{eq:in}
 \infer={\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_2\}}{\type{ \ActS_2', \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{ \INT_2'}}}
{
  \infer
{\judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{\tilde{x}}.P_1 }{\type{\ActS_2, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST}}{ \INT_2}}}
{\judgebis{\env{\Gamma, \tilde{x}:\tilde{\capab}}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}}}
\end{equation}
where Lemma~\ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS \subseteq \ActS_1' \cup \ActS_2', \cha^p:!(\tilde{\capab}).{\ST}, \cha^{\overline{p}}:?(\tilde{\capab}).\overline{\ST} $, $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, and $ \INT \sqsubseteq \INT_1 \uplus \INT_2$.

Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\tilde{c}}{\tilde{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}$ with $\tilde{e} \downarrow \tilde{c}$. Moreover by Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}  we obtain the following type derivation:
 $$
\infer={\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}\big\} }{ \type{\ActS'}{\INT}}}
{\infer
{
\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}} {\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
{\infer={\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1\}}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}}}
{
\judgebis{\env{\Gamma}{ \Theta}}{P_1}{\type{\ActS_1, \cha^p:\ST}{\INT_1}}}
   &
\infer={\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{\tilde{c}\,}{\tilde{x}}\}}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}}}{
\judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\tilde{c}\,}{\tilde{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}} }}}
$$ 
Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST}$ is balanced as well; this concludes the proof for this case.

%%%%%%%%%%%%%%%%% 
\paragraph{\bf Case \rulename{r:Pass}} $$E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}\pired E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{\,q}}{x}\}\big\}$$

By assumption we have  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}$ with $\ActS$ balanced. Using   Lemma \ref{lem:context} ($\Leftarrow$) and inversion on rules \rulename{t:Par}, \rulename{t:Cat}, and \rulename{t:Thr} we infer:
$$
\infer=
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}}
{\infer
	{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{\overline{p}}}.P_1\} \para  D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'}{\INT'}}}
	{
	(\ref{eq:throw})
	&
	(\ref{eq:catch})
	}}
$$
where (\ref{eq:throw}) and (\ref{eq:catch}) correspond to the subtrees:
\begin{equation}\label{eq:throw}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} }{ \type{\ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT'_1}}}
		{\infer
{\judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^p}{\cha_1^{q}}.P_1}{\type{\ActS_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT_1}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:\overline{\STT}}{ \INT_1}} 
		}}
\end{equation}
\begin{equation}\label{eq:catch}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{ D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2}}}
		{\infer
{\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\overline{p}}}{x}.P_2 }{\type{\ActS_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT_2}}}
{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\STT, x:\ST}{\INT_2}}}	
}
\end{equation}
and where by Lemma \ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS' \subseteq \ActS$ and $\ActS' = \ActS'_1 \cup \ActS'_2,  \cha^p:!(\ST).\overline{\STT}, \cha_1^q:\ST, \cha^{\overline{p}}:?(\ST).\STT$. Moreover we have $\INT_1 \sqsubseteq \INT_1'$, $\INT_2 \sqsubseteq \INT_2'$, $\INT' \sqsubseteq \INT$ and $\INT' = \INT'_1 \addelta \INT'_2$. Notice that as $\ActS$ is balanced, in $\ActS$ there is a $\cha_1^{\overline{q}}:\overline{\ST}$.

Then by Lemma \ref{lem:substitution}(\ref{subchavar}) we have $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha_1^q}{x}}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}$ thus obtaining the following typing tree where we have used Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}, we also use the following subtree:
\begin{equation}\label{eq:pass}
 \infer=
		{\judgebis{\env{\Gamma}{\Theta}}{ D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}}
		{\judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\cha_1^{q}}{x}}{\type{\ActS_2, \cha^+:\STT, \cha_1^q:\ST}{\INT_2}}	
}
\end{equation}
$$
\infer=
	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}\big\}}{ \type{\ActS''}{\INT}}}
{\infer
	{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}}}
	{\infer=
		{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} }{ \type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1}}}
		{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:\overline{\STT}}{ \INT_1}} 
		}
	& (\ref{eq:pass})
	}}
$$
Notice that by construction $\ActS''$ is balanced. It is also important to see how the contexts $C^{-}$ and $D^{+}$ correctly implement the fact that the number of active sessions is changed after delegating session $\kappa_1$ to process $P_2$.
 This concludes the proof for this case.


% 
\paragraph{\bf Cases \rulename{r:IfTr} and \rulename{r:IfFa}} Follows by an ease induction on the derivation tree.

% 
\paragraph{\bf Case \rulename{r:Close}} This case follows the same reasoning as in  \rulename{r:Open} case.
% 
\paragraph{\bf Case \rulename{r:Branch}} This case is similar to  previous \rulename{r:I/O} case. 
% 
\paragraph{\bf Case \rulename{r:Str}} Follows from Theorem~\ref{th:congr} (Subject Congruence).
% 
\paragraph{\bf Case \rulename{r:Par}} Follows by induction and by applying rule $\rulename{t:Par}$.
%
\paragraph{\bf Case \rulename{r:Res}} Follows by induction and by the fact that  $\ActS$ is balanced. Indeed, by hypothesis and by inversion on rule \rulename{t:CRes} all the occurences of bracketed assignements ($[\cha^p:\ST]$) are necessarily balanced thus making it possible to apply the inductive hypothesis to the premise of the rule and concluding the analysis of this case and the proof of the theorem.
% \end{description}
\end{proof}

We are now ready to state our first main result:
 the \emph{absence of communication errors} for well-typed processes.
Recall that our notion of error process has been given in 
Definition~\ref{d:kred}.


\begin{theorem}[Typing Ensures Safety]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ never reduces into an error.
\end{theorem}

\begin{proof}
We assume, towards a contradiction, that there exists a $P_1$ 
such that ~$P \pired^* P_1$ and $P_1$ is an error process.
By Theorem~\ref{th:subred} (Subject Reduction), $P_1$ is well-typed under a balanced typing $\D_1$.
Following Def.~\ref{d:kred}, there are two possibilities for $P_1$, namely 
it contains %(i)  exactly one $\kappa$-process, 
(i) exactly two $\kappa$-processes which do not form a $\kappa$-redex and (ii) three or more $\kappa$-processes.
Consider the second possibility.   
There are several combinations;
by inversion on rule \rulename{t:CRes}
we have that,
for some session types $\alpha_1$ and $\alpha_2$,
% either $\{\kappa^{p}: \alpha_1, \kappa^{\overline{p}}: \alpha_2\} \subseteq \D_1$ or  
$\{[\kappa^{p}: \alpha_1], [\kappa^{\overline{p}}: \alpha_2]\} \subseteq  \D_1$. 
In all cases, since the two $\kappa$-processes do not form a $\kappa$-redex then, necessarily, 
 $\alpha_1 \neq \overline{\alpha_2}$. This, however, contradicts the definition of balanced typings (Def.~\ref{d:balanced}).
The second possibility again contradicts Def.~\ref{d:balanced}, 
as in that case $\D_1$ would capture the fact that
at least one $\kappa$-process does not have a complementary partner for forming a $\kappa$-redex.
We thus conclude that well-typed processes never reduce to an error.
\end{proof}


\subsection{Session Consistency}\label{ss:consist}

We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
Informally, %we say that a %session on channel $\kappa$ 
a process $P$
is called \emph{consistent} 
if %it is never disrupted by an evolvability step. 
%That is, 
whenever  %session on $\kappa$ is active and 
it has 
a $\kappa$-redex (cf. Def.~\ref{d:kred}) then 
possible interleaved update actions do not destroy such a redex.
%performing an update action does not affect the behavior of active sessions.

Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$, possibly followed
by uses of rules $\rulename{r:Res}$, $\rulename{r:Str}$, and $\rulename{r:Par}$.
We then define:

%\begin{definition}[Session Consistency]\label{d:consist}
%Let $P$ be a process. 
%A session on channel $\kappa$ is \emph{consistent} in $P$ if,
%for all process $P', P''$ and contexts $E, C, D$ 
%such that 
%$$P \pired^{*} P' \equiv (\nu \tilde{\kappa})E\big\{C\{P_1\} \para  D\{P_2\}\big\}$$
%where $P_1$ and $P_2$ make $P'$ a $\kappa$-redex
%and $P' \pired_{\text{upd}} P''$, then there exist contexts $E', C'$, and $D'$ such that
%$$P'' \equiv (\nu \tilde{\kappa})E'\big\{C'\{P_1\} \para  D'\{P_2\}\big\}$$
%\end{definition}
%
%Hence, consistency on a session $\kappa$ %as formalized by Def.~\ref{d:consist} 
%says that update actions do not destroy $\kappa$-redexes. 
%Clearly, this definition does not rule out the possibility of interleaving intra-session communication 
%and update steps: it just requires update actions to reconfigure parts of the system not currently engaged into active sessions. 
%We find that giving priority to disciplined structured behavior over 
%runtime adaptation steps, as intended by this notion of consistency, 
%is a rather natural requirement.
%
%\jp{I feel consistency should be a property of processes, and focused on what the updates preserve
%rather than on what the sessions do. Hence I suggest stating consistency as:}

\begin{definition}[Consistency]\label{d:consis}
A process $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}

Recall that a \emph{located} $\kappa$-redex is a $\kappa$-redex in which one or both of
its constituting $\kappa$-processes are contained by least one located process.
This way, for instance, 
$$
\begin{array}{c}
\scomponent{l_2}{\,\scomponent{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1}  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2\,} \\
\scomponent{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1}  \para \scomponent{l_2}{\outC{\kappa^{\,\overline{p}}}{v}.P_2} \\
\scomponentbig{l_1}{\inC{\kappa^{\,p}}{\tilde{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2} 
\end{array}
$$
are located $\kappa$-redexes, whereas $\inC{\kappa^{\,p}}{\tilde{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2$ is not.
From the point of view of consistency, the distinction between located and unlocated $\kappa$-redexes is relevant:
since update actions result from synchronizations on located processes, 
unlocated $\kappa$-redexes are always preserved by update actions, 
whereas located $\kappa$-redexes may be destroyed by a  update action.
We have the following auxiliary proposition.

\begin{proposition}\label{p:nonzero}
Let 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced, 
be a well-typed process containing  
a $\kappa$-redex, for some $\kappa$. We have:
\begin{enumerate}[(a)]
\item $\ActS = \ActS', \kappa^p: \ST,  \kappa^{\overline{p}}:\overline{\ST}$
~~or~~ $\ActS = \ActS', [\kappa^p: \ST],  [\kappa^{\overline{p}}:\overline{\ST}]$
, for some session type $\ST$, and a balanced $\ActS'$.
\item If the $\kappa$-redex is located, then the runtime annotation for the location(s) hosting its 
constituting $\kappa$-processes is different from zero.
\end{enumerate}

\begin{proof}
Part~(a) is immediate from our definition of typing judgment, in particular from the fact that typing $\D$
records the types of currently active sessions, as implemented by channels such as $\kappa$.
Part~(b) follows directly by definition of typing rule \rulename{t:Loc} and part (a), observing that typing relies on the cardinality of $\D$
to compute (non zero) runtime annotations for locations. 
% and the fact that $\kappa$-redexes are essentially dual active sessions recorded in $\D$.
\end{proof}

\end{proposition}

\begin{theorem}[Typing Ensures Update Consistency]\label{t:consist}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced,
then $P$ is update consistent.
\end{theorem}

\begin{proof}
%By contradiction.
We assume, towards a contradiction, that there exist $P_1$, $P_2$, and $\kappa_1$ such that
(i)~$P~\pired^*~P_1$, (ii)~$P_1$ has a $\kappa_1$-redex,  (iii)~$P_1 \pired_{\text{upd}} P_2$, and 
(iv)~$P_2$ does not have a $\kappa_1$-redex.  Without loss of generality, 
we suppose that the reduction $P_1 \pired_{\text{upd}} P_2$ is due to a synchronization on location $l_1 \in \T$.
Since the $\kappa_1$-redex is destroyed by the update action from $P_1$ to $P_2$, the $\kappa_1$-redex in $P_1$ must necessarily be 
 a located $\kappa_1$-redex, i.e.,  in $P_1$, one or both $\kappa_1$-processes are contained inside $l_1$.
 Now, our reduction semantics (rule \rulename{r:Upd}) decrees that for such an update action to be enabled,
 the runtime annotation for $l_1$ in $P_1$ should be zero. However, by Theorem~\ref{th:subred} (Subject Reduction), we know that $P_1$ is well-typed under a balanced
 typing $\ActS_1$. Then, using well-typedness and Prop.~\ref{p:nonzero}(b)
we infer that the annotation for $l_1$ in $P_1$ must be different from zero: contradiction. 
Hence, update steps which destroy a  
$\kappa$-redex (located and unlocated) can never be enabled from a well-typed process 
  with a balanced typing (such as $P$) nor from any of its derivatives (such as $P_1$). We thus conclude that
  well-typedness implies update consistency.
\end{proof}

%\begin{proof}[Proof (Sketch)]
%Suppose $P$ reduces to a $P'$ 
%which contains a  $\kappa$-redex. 
%Subject reduction ensures that well-typedness under balanced typings is preserved by reduction.
%Therefore, $P'$ we have 
%$\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS', \kappa^p: \ST, \kappa^{\overline{p}}:\overline{\ST}}{\INT'}}$
%for some $\ST, \INT'$
%and 
%balanced typing $\Delta'$. (The assignments could be bracketed, this is for simplicity.)
%Suppose further that a reduction $P'  \pired_{\text{upd}} P''$ is enabled.
%There are two cases.
%First, the update concerns a location which does not contain none of the $\kappa$-processes.
%That is, the update is external to this $\kappa$-redex.
%We observe that the reduction to $P''$ poses no danger for the $\kappa$-processes: 
%if the update is enabled then the runtime annotation for the location 
%to be updated must be 0. Recall this annotation is maintained by typing based on $\D$.
%In fact, this update preserves \emph{all} $\kappa$-redexes in $P'$.
%Second, the update concerns a location in which one or both $\kappa$-processes are contained.
%This case is not possible:
%because typing ensures that location annotations correspond to the number of open sessions at such a location, 
%since $\kappa$-processes are declared in $\D$ the annotation for the involved location is greater than 0 and so the update cannot be enabled, because of \rulename{r:Upd}.
%\end{proof}


%We can show that all sessions in our well-typed processes are consistent. 
%We can indeed state:
%
%\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
%Suppose %\\%$P$ be a well-typed process. 
%$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $
%is a well-typed process.
%Then every session $\ST_\qua \in \INT$ %that can be established along the evolution of $P$, we have that 
%is consistent, in the sense of Def.~\ref{d:consist}.
%\end{corollary}
%
%This result follows from Thm.~\ref{th:subred} 
%by observing that 
%enabling update actions only for 
%located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
%rules out the possibility of 
%updating a location containing 
%a communicating process $P_{\langle c \rangle}$, as defined above.
%Indeed, our type system ensures that the annotations enabling update actions 
%are correctly assigned and maintained along reduction.



